\begin{tabbing}
ESAxioms\{i:l\}($E$;$T$;$M$;${\it loc}$;${\it kind}$;${\it val}$;${\it when}$;${\it after}$;${\it time}$;${\it sends}$;${\it sender}$;${\it index}$;${\it first}$;${\it pred}$;${\it causl}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$e$, ${\it e'}$:$E$. (${\it loc}$($e$) = ${\it loc}$(${\it e'}$)) $\Rightarrow$ ((${\it causl}$($e$,${\it e'}$)) $\vee$ ($e$ = ${\it e'}$) $\vee$ (${\it causl}$(${\it e'}$,$e$))))\+
\\[0ex]\& ($\forall$$e$:$E$. ($\uparrow$(${\it first}$($e$))) $\Leftarrow\!\Rightarrow$ ($\forall$${\it e'}$:$E$. (${\it loc}$(${\it e'}$) = ${\it loc}$($e$)) $\Rightarrow$ ($\neg$(${\it causl}$(${\it e'}$,$e$)))))
\\[0ex]\& (\=$\forall$$e$:$E$.\+
\\[0ex]($\neg$($\uparrow$(${\it first}$($e$))))
\\[0ex]$\Rightarrow$ \=(${\it loc}$(${\it pred}$($e$)) = ${\it loc}$($e$) \& ${\it causl}$(${\it pred}$($e$),$e$)\+
\\[0ex]\& ($\forall$${\it e'}$:$E$. (${\it loc}$(${\it e'}$) = ${\it loc}$($e$)) $\Rightarrow$ ($\neg$(${\it causl}$(${\it pred}$($e$),${\it e'}$) \& ${\it causl}$(${\it e'}$,$e$))))))
\-\-\\[0ex]\& (\=$\forall$$e$:$E$.\+
\\[0ex]($\neg$($\uparrow$(${\it first}$($e$))))
\\[0ex]$\Rightarrow$ ($\forall$$x$:Id, $t$:$\mathbb{Q}$. ${\it when}$($x$,$e$,$t$) = ${\it after}$($x$,${\it pred}$($e$),$t$ + ((${\it time}$($e$)) {-} (${\it time}$(${\it pred}$($e$)))))))
\-\\[0ex]\& Trans($E$;$e$,${\it e'}$.${\it causl}$($e$,${\it e'}$))
\\[0ex]\& SWellFounded(${\it causl}$($e$,${\it e'}$))
\\[0ex]\& (\=$\forall$$e$:$E$.\+
\\[0ex]($\uparrow$isrcv(${\it kind}$($e$)))
\\[0ex]$\Rightarrow$ (\=(${\it sends}$(lnk(${\it kind}$($e$)),${\it sender}$($e$)))[(${\it index}$($e$))]\+
\\[0ex]=
\\[0ex]msg(lnk(${\it kind}$($e$));tag(${\it kind}$($e$));${\it val}$($e$))))
\-\-\\[0ex]\& ($\forall$$e$:$E$. ($\uparrow$isrcv(${\it kind}$($e$))) $\Rightarrow$ (${\it causl}$(${\it sender}$($e$),$e$)))
\\[0ex]\& (\=$\forall$$e$, ${\it e'}$:$E$.\+
\\[0ex](${\it causl}$($e$,${\it e'}$))
\\[0ex]$\Rightarrow$ \=((($\neg$($\uparrow$(${\it first}$(${\it e'}$)))) c$\wedge$ ((${\it causl}$($e$,${\it pred}$(${\it e'}$))) $\vee$ ($e$ = ${\it pred}$(${\it e'}$))))\+
\\[0ex]$\vee$ (($\uparrow$isrcv(${\it kind}$(${\it e'}$))) c$\wedge$ ((${\it causl}$($e$,${\it sender}$(${\it e'}$))) $\vee$ ($e$ = ${\it sender}$(${\it e'}$))))))
\-\-\\[0ex]\& ($\forall$$e$:$E$. ($\uparrow$isrcv(${\it kind}$($e$))) $\Rightarrow$ (${\it loc}$($e$) = destination(lnk(${\it kind}$($e$)))))
\\[0ex]\& ($\forall$$e$:$E$, $l$:IdLnk. ($\neg$(${\it loc}$($e$) = source($l$))) $\Rightarrow$ (${\it sends}$($l$,$e$) = []))
\\[0ex]\& (\=$\forall$$e$, ${\it e'}$:$E$.\+
\\[0ex]($\uparrow$isrcv(${\it kind}$($e$)))
\\[0ex]$\Rightarrow$ ($\uparrow$isrcv(${\it kind}$(${\it e'}$)))
\\[0ex]$\Rightarrow$ (lnk(${\it kind}$($e$)) = lnk(${\it kind}$(${\it e'}$)))
\\[0ex]$\Rightarrow$ \=((${\it causl}$($e$,${\it e'}$))\+
\\[0ex]$\Leftarrow\!\Rightarrow$ \=((${\it causl}$(${\it sender}$($e$),${\it sender}$(${\it e'}$)))\+
\\[0ex]$\vee$ (${\it sender}$($e$) = ${\it sender}$(${\it e'}$) \& ((${\it index}$($e$)) $<$ (${\it index}$(${\it e'}$)))))))
\-\-\-\\[0ex]\& (\=$\forall$$e$:$E$, $l$:IdLnk, $n$:\{0..$\parallel$${\it sends}$($l$,$e$)$\parallel^{-}$\}.\+
\\[0ex]$\exists$\=${\it e'}$:$E$\+
\\[0ex](($\uparrow$isrcv(${\it kind}$(${\it e'}$))) c$\wedge$ (lnk(${\it kind}$(${\it e'}$)) = $l$ \& ${\it sender}$(${\it e'}$) = $e$ \& ${\it index}$(${\it e'}$) = $n$)))
\-\-\-
\end{tabbing}